es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id },
Q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
[e1,e2]~([a,b].Q(a,b))+  e1  e2  

latex

Definitions	x(s1,s2), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x:A. B(x), P  Q, t  T, loc(e), Id, E, x,y. t(x;y), [e1,e2]~([a,b].p(a;b))+, e  e' , Prop, ES
Lemmas	es-pstar-q-le, event system wf, es-pplus wf, es-E wf, Id wf, es-loc wf